package systemf

/**
   * adapted from parser for untyped lambda calculus by Miles Sabin 
   */


trait AST { 

     type VarRef

}


sealed trait LTerm extends AST{
  type VarRef = Int
  def toString_(ctx: Context) : String = toString
}

trait BaseValue extends LTerm {
  def baseType():BaseType
}


 case class Tru extends LTerm with BaseValue{
   override def toString = "true"
   override def baseType = TyBool
 }
 case class Fls extends LTerm with BaseValue{
   override def toString= "false"
   override def baseType = TyBool
 }
 case class Unit extends LTerm with BaseValue{
   override def toString = "unit"
   override def baseType = TyUnit
 }
 case class Lit(n: int) extends LTerm with BaseValue{
   override def toString = n.toString
   override def baseType = TyInt
 }
 
 case class If(cond: LTerm, pos: LTerm, neg: LTerm) extends LTerm {
   override def toString_(ctx: Context) = {
     "if "+cond.toString_(ctx)+" then "+pos.toString_(ctx)+" else "+neg.toString_(ctx)
   }
 }

 
 

 case class Var(n: Int) extends LTerm  {
   override def toString_(ctx: Context) = ctx(n) match {case b:Some[NameBinding] => b.get.name}
 }
 
 case class Lam(x: String, ty: LType, t:LTerm) extends LTerm {
   override def toString_(ctx: Context) = {
     val (ctx2, x2) = ctx.pickDisplayName(x)
     "(λ"+x2+":"+ty.toString_(ctx)+" ."+t.toString_(ctx2)+")"
   }
 }
 
 case class App(t1:LTerm, t2:LTerm) extends LTerm {
   override def toString_(ctx: Context) = 
     "APP("+t1.toString_(ctx) + " " + t2.toString_(ctx) + ")"
 }
 

 //TVar -> see TyVar
 case class TLam(x: String, t:LTerm) extends LTerm {
   override def toString_(ctx: Context) = {
     val (ctx2, x2) = ctx.pickDisplayNameType(x)
     "(Λ"+x2+" ."+t.toString_(ctx2)+")"
   }
 }
   

 case class TApp(t1:LTerm, ty: LType) extends LTerm {
   override def toString_(ctx: Context) = 
     "TAPP("+t1.toString_(ctx) + " [" + ty.toString_(ctx) + "])"
 }
 
 case class Pack(ty:LType, t:LTerm, pubty:LType) extends LTerm {
   override def toString_(ctx: Context) = 
     "{*"+ty.toString_(ctx) + ", "+t.toString_(ctx) +" } as "+ pubty.toString_(ctx)
 }
 
 case class Unpack(impl: LTerm, pubty:String,pubvar:String, body:LTerm) extends LTerm {
   override def toString_(ctx: Context) = {
     val (ctxtype, pubty_) = ctx.pickDisplayNameType(pubty)
     val (ctxtypeandvar, pubvar_) = ctxtype.pickDisplayName(pubvar)
     "import " + impl.toString_(ctx) + "into {"+pubty_ +", "+pubvar_ +"} in "+body.toString_(ctxtypeandvar)
   }
 }
 
 
 case class Let(n: VarName, t1: LTerm, t2: LTerm) extends LTerm {
   override def toString_(ctx:Context) = {
     val (ctx2, x2) = ctx.pickDisplayName(n.n)
     "let "+x2+" = " +t1.toString_(ctx) + " in " +(t2).toString_(ctx2)
   }
   override def toString = "let "+n+" = "+t1+" in "+t2
 }
 
 
 case class Record(fields: List[(String,LTerm)]) extends LTerm {
   override def toString_(ctx: Context) = 
     "{" + fields.foldRight("")({case ((s,t),xs) => s +"="+ t.toString_(ctx) +", "+ xs} )+ "}"
   override def toString = "{" + fields.foldRight("")({case ((s,t),xs) => s +"="+ t +", "+ xs} )+ "}"
   def map[R](f:LTerm=>R):List[(String,R)] =
     fields.map({case (label,fld)=> (label,f(fld))})
 }
 case class RecProj(t: LTerm, label: String) extends LTerm {
   override def toString_(ctx: Context) = "from " + t.toString_(ctx) +" fld "+label
 }
 

 
 

 
 
 
 
 abstract class Named(n:String) extends LTerm 
 case class VarName(n: String) extends Named(n) {
   override def toString = n
 }
 case class TyVarName(n: String) extends Named(n)with LType {
   override def toString = n
 }
 /*
 case class Ref(n: Named) extends LTerm {
   def value = n
 }
 */

 case class Lambda(n: VarName,ty: LType, t: LTerm) extends LTerm 
 {
   override def toString = "(λ"+n+":"+ty+" ."+t+")"
 }
 case class TyLambda(n: TyVarName,t: LTerm) extends LTerm 
 {
   override def toString = "(Λ"+n+ t+")"
 } 
  
 case class Applic(t1: LTerm, t2: LTerm) extends LTerm 
 {
   override def toString = "("+t1+" "+t2+")"
 } 
 
 case class TyApplic(t: LTerm, ty: LType) extends LTerm 
 {
   override def toString = "("+t + " [" + ty+ "] )"
 }
  
 case class Import(impl: LTerm, pubty:TyVarName,pubvar:VarName, body:LTerm) extends LTerm {
   override def toString_(ctx: Context) = 
     "import " + impl.toString_(ctx) + "into {"+pubty+ ", "+pubvar +"} in "+body.toString_(ctx)
 }
 
 
 
 
 
 
 
 

 sealed trait LType extends LTerm 
 
 trait BaseType extends LType {
   val name: String
   override def toString_(ctx: Context) = name
   override def toString = name
 }
 
 case class TyBool() extends LType with BaseType
 { val name="Bool" }
 case class TyInt()  extends LType with BaseType
 { val name="Int"  }
 case class TyTop()  extends LType with BaseType
 { val name="Top"  }
 case class TyUnit() extends LType with BaseType
 { val name="Unit" }

 case class TyArr(t1: LType, t2: LType) extends LType {
   override def toString_(ctx: Context) = 
             "("+t1.toString_(ctx) +" => " +t2.toString_(ctx)+")"
   override def toString = "("+t1 +" => " +t2+")"
   def map(f:LType=>LType):TyArr=
      TyArr(f(t1), f(t2))
 }
 
 case class TyVar(n: Int) extends LType 
 { 
   override def toString_(ctx: Context) = ctx(n) match {case b:Some[TypeVarBinding] => n+"="+b.get.name}
   
   override def toString = "TV("+n.toString+")"
 }
 
 


 

 case class TyRecord(fields: List[(String,LType)]) extends LType {
   override def toString = "{" + fields.foldRight("")({case ((s,t),xs) => s +":"+ t +", "+ xs} )+ "}"
   def map[R](f:LType=>R):List[(String,R)] =
       fields.map({case (label,fld)=> (label,f(fld))})
   def field(label:String) = {
       val results = fields.filter( {case (fldlabel,fldtype) => label == fldlabel}).map(_ _2)
       if (results.length == 0)throw new TypeExc("no label "+label+" in record")
       if (results.length >1  )throw new TypeExc("multiple labels "+label+" in record")
       results.head
   }
 }
 
 
 case class TyUniv(x: String, ty: LType) extends LType  {
   override def toString_(ctx: Context) =  {
     val (ctx2, x2) = ctx.pickDisplayNameType(x)
    "forall "+x2+" ."+ty.toString_(ctx2)+""
   }
   override def toString = "forall "+x +". "+ty
   override def equals(o: Any) = o match {
     case TyUniv(ox,oty) => ty == oty
     case _ => false
 }
 }

 case class TyExist(x:String, ty: LType) extends LType {
   override def toString_(ctx: Context) = {
     val (ctx2, x2) = ctx.pickDisplayNameType(x)
     "{forsome "+x2+" ,"+ty.toString_(ctx2)+"}"
   }
   override def toString = "{forsome "+x+","+ty+"}"
   override def equals(o: Any) = o match {
     case TyExist(ox,oty) => ty == oty
     case _ => false
   }
   
 }
 
 case class TyExistential(x: TyVarName, ty: LType) extends LType {
   override def toString_(ctx: Context) = "forsome"+x+". "+ty.toString_(ctx)
   override def toString = "forsome "+x +","+ty
 }

 case class TyUniversal(x: TyVarName,ty: LType) extends LType {
   override def toString_(ctx: Context) = "forall"+x+". "+ty.toString_(ctx)
   override def toString = "forall"+x +". "+ty
 }
 
 
 


 

